Search for: All records

Recent work has found that adversarially-robust deep networks used for image classification are more interpretable: their feature attributions tend to be sharper, and are more concentrated on the objects associated with the image’s ground- truth class. We show that smooth decision boundaries play an important role in this enhanced interpretability, as the model’s input gradients around data points will more closely align with boundaries’ normal vectors when they are smooth. Thus, because robust models have smoother boundaries, the results of gradient- based attribution methods, like Integrated Gradients and DeepLift, will capture more accurate information about nearby decision boundaries. This understanding of robust interpretability leads to our second contribution: boundary attributions, which aggregate information about the normal vectors of local decision bound- aries to explain a classification outcome. We show that by leveraging the key fac- tors underpinning robust interpretability, boundary attributions produce sharper, more concentrated visual explanations{—}even on non-robust models. 

As Internet-of-Things (IoT) devices rapidly gain popularity, they raise significant privacy concerns given the breadth of sensitive data they can capture. These concerns are amplified by the fact that in many situations, IoT devices collect data about people other than their owner or administrator, and these stakeholders have no say in how that data is managed, used, or shared. To address this, we propose a new model of ownership, IoT Ephemeral Ownership (TEO). TEO allows stakeholders to quickly register with an IoT device for a limited period, and thus claim co-ownership over the sensitive data that the device generates. Device admins retain the ability to decide who may become an ephemeral owner, but no longer have access or control to the private data generated by the device. The encrypted data in TEO is accessible only by entities after seeking explicit permission from the different co-owners of that data. We verify the key security properties of our protocol underpinning TEO in the symbolic model using ProVerif. We also implement a cross-platform prototype of TEO for mobile phones and embedded devices, and integrate it into three real-world application case studies. Our evaluation shows that the latency and battery impact of TEO is typically small, adding ≤ 187 ms onto one-time operations, and introducing limited (<25%) overhead on recurring operations like private data storage. 

We turn the definition of individual fairness on its head - rather than ascertaining the fairness of a model given a predetermined metric, we find a metric for a given model that satisfies individual fairness. This can facilitate the discussion on the fairness of a model, addressing the issue that it may be difficult to specify a priori a suitable metric. Our contributions are twofold:First, we introduce the definition of a minimal metric and characterize the behavior of models in terms of minimal metrics. Second, for more complicated models, we apply the mechanism of randomized smoothing from adversarial robustness to make them individually fair under a given weighted Lp metric. Our experiments show that adapting the minimal metrics of linear models to more complicated neural networks can lead to meaningful and interpretable fairness guarantees at little cost to utility.

 

One of the standard correctness criteria for gradual typing is the dynamic gradual guarantee, which ensures that loosening type annotations in a program does not affect its behavior in arbitrary ways. Though natural, prior work has pointed out that the guarantee does not hold of any gradual type system for information-flow control. Toro et al.'s GSLRef language, for example, had to abandon it to validate noninterference. We show that we can solve this conflict by avoiding a feature of prior proposals: type-guided classification, or the use of type ascription to classify data. Gradual languages require run-time secrecy labels to enforce security dynamically; if type ascription merely checks these labels without modifying them (that is, without classifying data), it cannot violate the dynamic gradual guarantee. We demonstrate this idea with GLIO, a gradual type system based on the LIO library that enforces both the gradual guarantee and noninterference, featuring higher-order functions, general references, coarsegrained information-flow control, security subtyping and first-class labels. We give the language a domain-theoretic semantics, using Pitts' framework of relational structures to prove noninterference and the dynamic gradual guarantee.